natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
(2,1)-quasitopos?
structures in a cohesive (∞,1)-topos
In Awodey 09, Awodey 10 was first expressed the idea that dependent type theory with intensional identity types (Martin-Löf dependent type theory), viewed as homotopy type theory, is in similar relation to the concept of (∞,1)-toposes as extensional type theory is to the ordinary concept of toposes (as discussed at relation between type theory and category theory).
From Awodey 09, p. 13, Awodey 10, p. 15:
The homotopy interpretation of Martin-Löf type theory into Quillen model categories, and the related results on type-theoretic constructions of higher groupoids, are analogous to basic results interpreting extensional type theory and higher-order logic in (1-)toposes, and clearly indicate that the logic of higher toposes, and therewith of higher homotopy theory, is a form of intensional type theory.
A concise re-statement would be that:
the internal logic of (∞,1)-toposes is univalent homotopy type theory
(though there is fine print involved, e.g. the initiality conjecture);
there is a model of (univalent) homotopy type theory in any -topos
(this version has a proof, see below);
homotopy type theory is synthetic homotopy theory
(this may be read as a suggestive colloquial version of the previous statement, remaining vague on whether univalence is considered or not).
Following this suggestion, the weaker form of this idea, ignoring the univalent type universe and relating to the broader class of locally Cartesian closed (∞,1)-categories, was stated more concretely as a conjecture in Joyal 11. For more precision see Kapulkin-Lumsdaine 16, p. 9.
Roughly, this is about the following table of correspondences (for more see at relation between type theory and category theory):
Fore more precision see Kapulkin-Lumsdaine 16, p. 9.
A proof of the weaker version of the conjecture, in form of the statement that every locally presentable locally Cartesian closed (∞,1)-category is presented by a suitable type theoretic model category which provides categorical semantics for homotopy type theory, was proven in Shulman 12, Example 2.16, following Cisinski 12.
Generalizing this to a proof of the full conjecture required finding “strict” models for the object classifier by strict type universes. A series of article (Shulman 12, Shulman 13) showed that this is possible in an increasing class of special cases.
A proof of the general case was finally announced in Shulman 19.
For more see at model of type theory in an (infinity,1)-topos.
The idea is due to
Steve Awodey, Homotopy and Type Theory, grant proposal project description (pdf)
Steve Awodey, Type theory and homotopy, in: Dybjer P., Lindström S., Palmgren E., Sundholm G. (eds.), Epistemology versus Ontology, Springer (2012) 183-201 arXiv:1010.1810, doi:10.1007/978-94-007-4435-6_9
A pronounced statement of the weaker version was highlighted in
and stated more precisely in
The proof of the weaker version of Awodey’s conjecture (that every locally Cartesian closed (∞,1)-category has a presentation by a suitable type-theoretic model category which provides categorical semantics for homotopy type theory) is due, independently, to
following
The proof of the stronger version (including univalent type universes modelling object classifier of (∞,1)-toposes) was found for the special case of (∞,1)-presheaf (∞,1)-toposes over elegant Reedy categories in
Michael Shulman, The univalence axiom for elegant Reedy presheaves, Homology, Homotopy and Applications Volume 17 (2015) Number 2 (arXiv:1307.6248, doi:10.4310/HHA.2015.v17.n2.a6)
A general proof was announced in
and appeared in
It is reviewed in:
Last revised on July 26, 2022 at 14:21:22. See the history of this page for a list of all contributions to it.